(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 467
Accept states: [468]
Transitions:
467→468[0_1|0]
467→467[1_1|0, 2_1|0, 3_1|0, 4_1|0, 5_1|0]
467→469[5_1|1]
467→487[5_1|1]
469→470[4_1|1]
470→471[3_1|1]
471→472[2_1|1]
472→473[1_1|1]
473→474[0_1|1]
474→475[5_1|1]
475→476[4_1|1]
476→477[3_1|1]
477→478[2_1|1]
478→479[1_1|1]
479→480[0_1|1]
480→481[1_1|1]
481→482[1_1|1]
482→483[5_1|1]
483→484[4_1|1]
484→485[3_1|1]
485→486[2_1|1]
486→468[1_1|1]
486→474[1_1|1]
486→492[1_1|1]
486→511[5_1|2]
486→529[5_1|2]
487→488[4_1|1]
488→489[3_1|1]
489→490[2_1|1]
490→491[1_1|1]
491→492[0_1|1]
492→493[5_1|1]
493→494[4_1|1]
494→495[3_1|1]
495→496[2_1|1]
496→497[1_1|1]
497→498[0_1|1]
498→499[5_1|1]
499→500[4_1|1]
500→501[3_1|1]
501→502[2_1|1]
502→503[1_1|1]
503→504[0_1|1]
504→505[1_1|1]
505→506[1_1|1]
506→507[5_1|1]
507→508[4_1|1]
508→509[3_1|1]
509→510[2_1|1]
510→468[1_1|1]
510→474[1_1|1]
510→492[1_1|1]
510→511[5_1|2]
510→529[5_1|2]
511→512[4_1|2]
512→513[3_1|2]
513→514[2_1|2]
514→515[1_1|2]
515→516[0_1|2]
516→517[5_1|2]
517→518[4_1|2]
518→519[3_1|2]
519→520[2_1|2]
520→521[1_1|2]
521→522[0_1|2]
522→523[1_1|2]
523→524[1_1|2]
524→525[5_1|2]
525→526[4_1|2]
526→527[3_1|2]
527→528[2_1|2]
528→480[1_1|2]
528→498[1_1|2]
528→553[5_1|2]
528→571[5_1|2]
529→530[4_1|2]
530→531[3_1|2]
531→532[2_1|2]
532→533[1_1|2]
533→534[0_1|2]
534→535[5_1|2]
535→536[4_1|2]
536→537[3_1|2]
537→538[2_1|2]
538→539[1_1|2]
539→540[0_1|2]
540→541[5_1|2]
541→542[4_1|2]
542→543[3_1|2]
543→544[2_1|2]
544→545[1_1|2]
545→546[0_1|2]
546→547[1_1|2]
547→548[1_1|2]
548→549[5_1|2]
549→550[4_1|2]
550→551[3_1|2]
551→552[2_1|2]
552→480[1_1|2]
552→498[1_1|2]
552→553[5_1|2]
552→571[5_1|2]
553→554[4_1|2]
554→555[3_1|2]
555→556[2_1|2]
556→557[1_1|2]
557→558[0_1|2]
558→559[5_1|2]
559→560[4_1|2]
560→561[3_1|2]
561→562[2_1|2]
562→563[1_1|2]
563→564[0_1|2]
564→565[1_1|2]
565→566[1_1|2]
566→567[5_1|2]
567→568[4_1|2]
568→569[3_1|2]
569→570[2_1|2]
570→504[1_1|2]
571→572[4_1|2]
572→573[3_1|2]
573→574[2_1|2]
574→575[1_1|2]
575→576[0_1|2]
576→577[5_1|2]
577→578[4_1|2]
578→579[3_1|2]
579→580[2_1|2]
580→581[1_1|2]
581→582[0_1|2]
582→583[5_1|2]
583→584[4_1|2]
584→585[3_1|2]
585→586[2_1|2]
586→587[1_1|2]
587→588[0_1|2]
588→589[1_1|2]
589→590[1_1|2]
590→591[5_1|2]
591→592[4_1|2]
592→593[3_1|2]
593→594[2_1|2]
594→504[1_1|2]